\documentclass[12pt]{report}
\usepackage[]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{fullpage}
\usepackage{coqdoc}
\usepackage{amsmath,amssymb}
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% This file has been automatically generated with the command
%% coqdoc -q -g --latex -o InstrEval.tex InstrEval.v 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\coqlibrary{InstrEval}{Library }{InstrEval}

\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Inductive} \coqdocvar{InstrEval} (\coqdocvar{st}: \coqdocvar{State}) : \coqdocvar{Instr} \ensuremath{\rightarrow} \coqdocvar{State} \ensuremath{\rightarrow} \coqdockw{Prop} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{skip\_eval} :\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{InstrEval} \coqdocvar{st} \coqdocvar{instr\_skip} \coqdocvar{st}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{assign\_bool\_eval} : \coqdockw{\ensuremath{\forall}} \coqdocvar{bid} \coqdocvar{bexp} \coqdocvar{b},\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{BoolEval} \coqdocvar{st} \coqdocvar{bexp} \coqdocvar{b} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} (\coqdocvar{instr\_assign\_bool} \coqdocvar{bid} \coqdocvar{bexp}) (\coqdocvar{Update} \coqdocvar{st} \coqdocvar{bid} (\coqdocvar{bool\_val} \coqdocvar{b}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{assign\_int\_eval} : \coqdockw{\ensuremath{\forall}} \coqdocvar{zid} \coqdocvar{zexp} \coqdocvar{z},\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ArithEval} \coqdocvar{st} \coqdocvar{zexp} \coqdocvar{z} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} (\coqdocvar{instr\_assign\_int} \coqdocvar{zid} \coqdocvar{zexp}) (\coqdocvar{Update} \coqdocvar{st} \coqdocvar{zid} (\coqdocvar{int\_val} \coqdocvar{z}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{assign\_byte\_eval} : \coqdockw{\ensuremath{\forall}} \coqdocvar{bid} \coqdocvar{bexp} \coqdocvar{b},\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ByteEval} \coqdocvar{st} \coqdocvar{bexp} (\coqdocvar{Some} \coqdocvar{b}) \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} (\coqdocvar{instr\_assign\_byte} \coqdocvar{bid} \coqdocvar{bexp}) (\coqdocvar{Update} \coqdocvar{st} \coqdocvar{bid} (\coqdocvar{byte\_val} \coqdocvar{b}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{assign\_matrix\_eval} : \coqdockw{\ensuremath{\forall}} \coqdocvar{mid} (\coqdocvar{m} \coqdocvar{n}: \coqdocvar{Integer}) (\coqdocvar{matr}: \coqdocvar{Matrix} \coqdocvar{Byte} \coqdocvar{m} \coqdocvar{n}) (\coqdocvar{mexp} : \coqdocvar{MatrixExp}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{MatrixEval} \coqdocvar{st} \coqdocvar{mexp} \coqdocvar{matr} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} (\coqdocvar{instr\_assign\_matrix} \coqdocvar{mid} \coqdocvar{mexp}) (\coqdocvar{Update} \coqdocvar{st} \coqdocvar{mid} (\coqdocvar{byte\_matrix\_val} \coqdocvar{matr}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{seq\_eval} : \coqdockw{\ensuremath{\forall}} \coqdocvar{i1} \coqdocvar{i2} \coqdocvar{st'} \coqdocvar{st'{}'},\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{InstrEval} \coqdocvar{st} \coqdocvar{i1} \coqdocvar{st'} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st'} \coqdocvar{i2} \coqdocvar{st'{}'} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} (\coqdocvar{instr\_seq} \coqdocvar{i1} \coqdocvar{i2}) \coqdocvar{st'{}'}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{if\_eval\_true} : \coqdockw{\ensuremath{\forall}} \coqdocvar{bexp} \coqdocvar{i1} \coqdocvar{i2} \coqdocvar{st'},\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{BoolEval} \coqdocvar{st} \coqdocvar{bexp} \coqdocvar{TRUE} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} \coqdocvar{i1} \coqdocvar{st'} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} (\coqdocvar{instr\_if} \coqdocvar{bexp} \coqdocvar{i1} \coqdocvar{i2}) \coqdocvar{st'}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{if\_eval\_false} : \coqdockw{\ensuremath{\forall}} \coqdocvar{bexp} \coqdocvar{i1} \coqdocvar{i2} \coqdocvar{st'},\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{BoolEval} \coqdocvar{st} \coqdocvar{bexp} \coqdocvar{FALSE} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} \coqdocvar{i2} \coqdocvar{st'} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} (\coqdocvar{instr\_if} \coqdocvar{bexp} \coqdocvar{i1} \coqdocvar{i2}) \coqdocvar{st'}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{while\_eval\_true} : \coqdockw{\ensuremath{\forall}} \coqdocvar{bexp} \coqdocvar{i} \coqdocvar{st'} \coqdocvar{st'{}'},\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{BoolEval} \coqdocvar{st} \coqdocvar{bexp} \coqdocvar{TRUE} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} \coqdocvar{i} \coqdocvar{st'} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st'} (\coqdocvar{instr\_while} \coqdocvar{bexp} \coqdocvar{i}) \coqdocvar{st'{}'} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} (\coqdocvar{instr\_while} \coqdocvar{bexp} \coqdocvar{i}) \coqdocvar{st'{}'}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{while\_eval\_false} : \coqdockw{\ensuremath{\forall}} \coqdocvar{bexp} \coqdocvar{i},\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{BoolEval} \coqdocvar{st} \coqdocvar{bexp} \coqdocvar{FALSE} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} (\coqdocvar{instr\_while} \coqdocvar{bexp} \coqdocvar{i}) \coqdocvar{st}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{for\_eval\_end} : \coqdockw{\ensuremath{\forall}} \coqdocvar{i} \coqdocvar{n} \coqdocvar{instr},\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{BoolEval} \coqdocvar{st} (\coqdocvar{bool\_exp\_ge} (\coqdocvar{arith\_exp\_id} \coqdocvar{i}) \coqdocvar{n}) \coqdocvar{TRUE} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} (\coqdocvar{instr\_for} \coqdocvar{i} \coqdocvar{n} \coqdocvar{instr}) \coqdocvar{st}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{for\_eval\_step} : \coqdockw{\ensuremath{\forall}} \coqdocvar{i} \coqdocvar{x} \coqdocvar{n} \coqdocvar{instr} \coqdocvar{st'} \coqdocvar{st'{}'},\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{BoolEval} \coqdocvar{st} (\coqdocvar{bool\_exp\_lt} (\coqdocvar{arith\_exp\_id} \coqdocvar{i}) \coqdocvar{n}) \coqdocvar{TRUE} \ensuremath{\rightarrow} \coqdocvar{InstrEval} \coqdocvar{st} \coqdocvar{instr} \coqdocvar{st'} \ensuremath{\rightarrow} \coqdoceol
\coqdocindent{3.00em}
\coqdocvar{InstrEval} \coqdocvar{st'} (\coqdocvar{instr\_for} \coqdocvar{i} \coqdocvar{n} \coqdocvar{instr}) \coqdocvar{st'{}'} \ensuremath{\rightarrow} \coqdocvar{st'} \coqdocvar{i} = \coqdocvar{Some} (\coqdocvar{int\_val} \coqdocvar{x}) \ensuremath{\rightarrow} \coqdocvar{st'{}'} \coqdocvar{i} = \coqdocvar{Some} (\coqdocvar{int\_val} (\coqdocvar{int\_plus} \coqdocvar{x} \coqdocvar{ONE})) \ensuremath{\rightarrow}\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{InstrEval} \coqdocvar{st} (\coqdocvar{instr\_for} \coqdocvar{i} \coqdocvar{n} \coqdocvar{instr}) \coqdocvar{st'{}'}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{matrix\_set\_eval} : \coqdockw{\ensuremath{\forall}} \coqdocvar{m} \coqdocvar{n} \coqdocvar{i} \coqdocvar{j} \coqdocvar{e1} \coqdocvar{e2} \coqdocvar{e} \coqdocvar{mid} (\coqdocvar{matr} \coqdocvar{matr'}: \coqdocvar{Matrix} \coqdocvar{Byte} \coqdocvar{m} \coqdocvar{n}) \coqdocvar{b},\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{MatrixEval} \coqdocvar{st} (\coqdocvar{matrix\_exp\_id} \coqdocvar{mid}) \coqdocvar{matr} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{st} \coqdocvar{e1} \coqdocvar{i} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{st} \coqdocvar{e2} \coqdocvar{j} \ensuremath{\rightarrow} \coqdocvar{ByteEval} \coqdocvar{st} \coqdocvar{e} (\coqdocvar{Some} \coqdocvar{b}) \ensuremath{\rightarrow} \coqdocvar{matrix\_set} \coqdocvar{matr} \coqdocvar{i} \coqdocvar{j} \coqdocvar{b} = \coqdocvar{Some} \coqdocvar{matr'} \ensuremath{\rightarrow}\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{InstrEval} \coqdocvar{st} (\coqdocvar{instr\_matrix\_set} \coqdocvar{mid} \coqdocvar{e1} \coqdocvar{e2} \coqdocvar{e}) (\coqdocvar{Update} \coqdocvar{st} \coqdocvar{mid} (\coqdocvar{byte\_matrix\_val} \coqdocvar{matr'}))\coqdoceol
\coqdocnoindent
.\coqdoceol
\end{coqdoccode}
\end{document}
